Inference at * 2 1 1 1 1 1 1 
Iof proof for Lemma less-fast-fib:



1. f : 
1. n, a, b:.
1. {m:| 
1. {k:. (a = fib(k))  ((k  0)  (b = 0))  ((0 < k)  (b = fib(k - 1)))  (m = fib(n+k))} 
2. n : 
3. v : 
4. k:. (1 = fib(k))  ((k  0)  (0 = 0))  ((0 < k)  (0 = fib(k - 1)))  (v = fib(n+k))
5. f(n,1,0) = v
  v = fib(n) 

latex

 by (InstHyp [0] (-2)) 
CollapseTHEN ((Auto) 
CollapseTHEN (Auto')) 

latex

C1: .....antecedent..... NILNIL

C1:   1 = fib(0)
C.

Definitions	#$n, , -n, n - m, s = t, T, True, A, False, Void, a < b, f(a), , fib(n), A  B, P  Q, n+m, x:A. B(x), x:AB(x), t  T, , {x:A| B(x)}
Lemmas	fib wf, nat wf, le wf